$\forall$${\it the\_w}$:World, $l$:IdLnk, ${\it mss}$:Msg List. withlnk($l$;${\it mss}$) $\in$ ($t$:Id$\times$${\it the\_w}$.M($l$,$t$)) List